$\forall$$T$, $A$:Type, $L$:$T$ List, $R$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow$Prop), $P$, $Q$:($A$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow$Prop).
\\[0ex](Trans $1$,$2$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $R$($1$,$2$))
\\[0ex]$\Rightarrow$ ($\forall$$x$:$A$. causal\_order($L$;$R$;$\lambda$$i$.$P$($x$,$i$);$\lambda$$i$.$Q$($x$,$i$)))
\\[0ex]$\Rightarrow$ causal\_order($L$;$R$;$\lambda$$i$.$\exists$$x$:$A$. $P$($x$,$i$);$\lambda$$i$.$\exists$$x$:$A$. $Q$($x$,$i$))